FDL - Nuprl Definition : poss-le

Nuprl Definition : poss-le

0,22

e2 == 1of(e1) = 1of(e2) & 1of(2of(e1))

1of(2of(e2))

clarification:

poss-le{i:l}(e1; e2) == 1of(e1) = 1of(e2)

ES{i} & es-le(1of(e1);1of(2of(e1));1of(2of(e2)))

Definitions A & B, s = t, ES, e e' , 1of(t), 2of(t)

FDL editor aliases poss-le

Definitions	A & B, s = t, ES, e e' , 1of(t), 2of(t)
FDL editor aliases	poss-le